es:ES, P, Q:(E), f1:({e:E| P(e)} {e:E| Q(e)} ), f2:({e:E| Q(e)} E).
(f1 is locl-pre-preserving on P & f2 is locl-pre-preserving on Q)
 f2 o f1 is locl-pre-preserving on P 

latex

Definitions	x:A. B(x), f is locl-pre-preserving on P, t  T, E, f(a), {x:A| B(x)} , x:AB(x), S  T, suptype(S; T), x:A  B(x), , P & Q, P  Q, Type, ES, f is R-pre-preserving on P, e loc e' , x.A(x)
Lemmas	rel-pre-preserving-compose, es-le wf, locl-pre-preserving wf